There is a trend in modern computing towards designing computer systems and computer code that is automatically verified prior to execution, to insure that the computer code is free from certain forms of coding errors, as well as that the computer code is not malicious in nature.
If an adversary succeeds in deceiving a user into executing malicious code, such as a virus or other undesired program, catastrophic consequences may result, including data theft, data destruction, and the like. Thus, it is important to develop methods that prevent malicious code from executing and causing harm to users and their data.
One means of preventing malicious code from executing is to shield the computer systems and the associated communications channels, peripherals, etc., using physical and logical access controls, such as locked doors to computer rooms, and password protected computer systems. Another means of preventing malicious code from executing is to use cryptographic authentication mechanisms to detect code that has not originated with a known and trusted code provider, or that has been tampered with. However, these means are not foolproof. If an intruder manages to penetrate the physical or logical security systems, and is able to present the computer system with malicious code that falsely authenticates itself as being uncompromised and originating from a trusted party, the malicious code will be allowed to execute, potentially causing great harm.
To provide a further line of defense, software developers have looked to means of securing the code itself, such that only non-malicious, “safe code” is allowed to execute. One means of securing the code involves inspecting and verifying that the code will not cause harm. The code is symbolically executed prior to being run. An analyzer follows the flow of all variables along all data paths in the program, and verifies that the code is “type safe.” This verification process is very time-consuming, and causes significant delays in the execution of the code.
Type safe code is code that does not allow the type system or type rules present in the code format to be violated. For example, storing values of a particular type into a variable defined as a different type is not allowed in type safe code. In addition, array bounds are enforced in type safe code. Assume an array is declared as having ten elements. A malicious code provider might wish to access array element eleven, thereby circumventing the type rules and gaining access to whatever variable happened to be located at the memory location corresponding to element eleven of the array—even if that variable is marked as being private or protected. Many exploits of security holes use this route, using a breach of type safety to modify variables that they normally would not have access to. Type safe code prevents this by disallowing the referencing of array elements beyond those defined to be in the array.
Another means for securing the code itself is disclosed in U.S. Pat. No. 6,128,774, issued to Necula et al. This means involves providing a proof accompanying the code, certifying that the code is safe. The proof is a series of hints that makes the verification analysis discussed above much faster. The code is inspected, just as with the verification methods discussed above. A verification condition is generated from the code. This verification condition is easier to generate than the full-blown control flow analysis discussed above. Once the verification condition is generated, the untrusted proof then tries to discharge the verification condition. If the proof discharges the condition, then the code is safe. If the proof fails to discharged the condition, then the safety of the code is still unknown. This method is faster than the detailed control flow verification discussed above, but it still requires that processing time be spent generating the verification condition from the code and discharging the verification condition using the proof, and it requires that bandwidth be spent on transmitting the proof. Thus, methods are needed to prevent malicious code from executing without expending valuable time and computer resources on dynamic code verification.